Table of Contents

1. Overview
2. Operation
   • Messages
   • Flags
   • Stylized Comments
     • Annotations
     • Control Comments
3. Abstract Types
   • Access
   • Mutability
   • Boulean Types
   • Primitive C Types
     • Characters
     • Enumerators
     • Numeric Types
     • Arbitrary Integral Types
4. Function Interfaces
   • Modifications
     • Special Modifications
     • Missing Modifies Clauses
     • Limitations
   • Global Variables
     • Controlling Globals Checking
   • Declaration Consistency
5. Memory Management
   • Storage Model
   • Deallocation Errors
     • Unshared References
     • Temporary Parameters
     • Owned and Dependent References
     • Kept Parameters
     • Stack References
     • Inner Storage
   • Implicit Memory Annotations
   • Reference Counting
6. Sharing
   • Aliasing
     • Unique Parameters
     • Returned Parameters
   • Exposure
     • Read-Only Storage
     • Exposed Storage
7. Value Constraints
   • Use Before Definition
     • Undefined Parameters
     • Relaxing Checking
     • Partially Defined Structures
     • Global Variables
   • Null Pointers
     • Predicate Functions
     • Overriding Null Types
     • Relaxing Null Checking
   • Execution
8. Special Clauses
9. Macros
   • Constant Macros
   • Function-like Macros
     • Side-Effect Free Parameters
     • Polymorphism
   • Controlling Macro Checking
   • Iterators
     • Defining Iterators
     • Using Iterators
10. Naming Conventions
    • Type-Based Naming Conventions
      • Czech Names
      • Slovak Names
      • Czechoslovak Names
    • Namespace Prefixes
    • Naming Restrictions
      • Reserved Names
      • Distinct Identifiers
11. Other Checks
    • Undefined Evaluation Order
    • Problematic Control Structures
      • Likely Infinite Loops
      • Switches
      • Deep Breaks
      • Loop and If Bodies
      • Complete if-else Logic
    • Suspicious Statements
      • Statements with No Effects
      • Ignored Return Values
    • Unused Declarations
    • Complete Programs
      • Unnecessary External Names
      • Declarations Missing from Headers
    • Compiler Limits

Figures

References
Acknowledgements